Resolutionsverfahren

Resolutionsverfahren,

 

Logik: ein Verfahren, mit dem festgestellt werden kann, ob aus den (prädikatenlogischen) Aussagen A₁,. .., A_n die Aussage K folgt. Hierzu werden A₁,. .., A_n und K in die Klauselform überführt, d. h. als Disjunktionen von negierten oder unnegierten Atomaussagen (Aussagen, die keine logische Partikel enthalten) dargestellt. Zu je zwei Klauseln wird eine Resolvente erzeugt, indem man ihre Disjunktion bildet und alle Paare der Form P ∨ ¬ P (P eine Atomaussage) weglässt. Ergibt sich als Resolvente die leere Klausel, so lag zuvor ein Widerspruch vor. Es gilt nun: Die Resolvente zweier Klauseln folgt logisch aus diesen (Korrektheit des Resolutionsverfahrens). Allerdings erzeugt das Resolutionsverfahren nicht alle möglichen Ableitungen aus den vorgegebenen Aussagen; es ist nicht vollständig. Wohl aber ist es widerlegungsvollständig, d. h., es liefert zu widersprüchlichen Voraussetzungen stets die leere Klausel als Resolvente (folgt also K aus A₁,. .., A_n, so ergibt sich zu A₁,. .., A_n ¬ K die leere Klausel als Resolvente). Das Resolutionsverfahren spielt eine wichtige Rolle in der maschinellen Logikverarbeitung und allgemein in der künstlichen Intelligenz.

 

Literatur:

 

E. Bergmann u. I. Noll: Mathemat. Logik mit Informatik-Anwendungen (1977);

 

Artificial intelligence, hg. v. P. H. Winston (Reading, Mass., ²1984).